Nuprl Definition : surject
13,42
postcript
pdf
Surj(
A
;
B
;
f
) ==
b
:
B
.
a
:
A
. (
f
(
a
) =
b
)
latex
clarification:
Surj(
A
;
B
;
f
) ==
b
:
B
.
a
:
A
. (
f
(
a
) =
b
B
)
latex
Up
fun
1
,
fun
1
Wellformedness Lemmas
surject
wf
,
surject
wf
Definitions
x
:
A
.
B
(
x
)
,
x
:
A
.
B
(
x
)
,
s
=
t
,
f
(
a
)
FDL editor aliases
surject
origin